Problem:
 terms(N) -> cons(recip(sqr(N)))
 sqr(0()) -> 0()
 sqr(s()) -> s()
 dbl(0()) -> 0()
 dbl(s()) -> s()
 add(0(),X) -> X
 add(s(),Y) -> s()
 first(0(),X) -> nil()
 first(s(),cons(Y)) -> cons(Y)

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {10,9,8,7,6}
   transitions:
    cons1(5) -> 10*
    cons1(12) -> 6*
    cons1(2) -> 10*
    cons1(4) -> 10*
    cons1(1) -> 10*
    cons1(3) -> 10*
    nil1() -> 10*
    s1() -> 11,9,8,7
    01() -> 11,8,7
    recip1(11) -> 12*
    sqr1(5) -> 11*
    sqr1(2) -> 11*
    sqr1(4) -> 11*
    sqr1(1) -> 11*
    sqr1(3) -> 11*
    terms0(5) -> 6*
    terms0(2) -> 6*
    terms0(4) -> 6*
    terms0(1) -> 6*
    terms0(3) -> 6*
    cons0(5) -> 1*
    cons0(2) -> 1*
    cons0(4) -> 1*
    cons0(1) -> 1*
    cons0(3) -> 1*
    recip0(5) -> 2*
    recip0(2) -> 2*
    recip0(4) -> 2*
    recip0(1) -> 2*
    recip0(3) -> 2*
    sqr0(5) -> 7*
    sqr0(2) -> 7*
    sqr0(4) -> 7*
    sqr0(1) -> 7*
    sqr0(3) -> 7*
    00() -> 3*
    s0() -> 4*
    dbl0(5) -> 8*
    dbl0(2) -> 8*
    dbl0(4) -> 8*
    dbl0(1) -> 8*
    dbl0(3) -> 8*
    add0(3,1) -> 9*
    add0(3,3) -> 9*
    add0(3,5) -> 9*
    add0(4,2) -> 9*
    add0(4,4) -> 9*
    add0(5,1) -> 9*
    add0(5,3) -> 9*
    add0(5,5) -> 9*
    add0(1,2) -> 9*
    add0(1,4) -> 9*
    add0(2,1) -> 9*
    add0(2,3) -> 9*
    add0(2,5) -> 9*
    add0(3,2) -> 9*
    add0(3,4) -> 9*
    add0(4,1) -> 9*
    add0(4,3) -> 9*
    add0(4,5) -> 9*
    add0(5,2) -> 9*
    add0(5,4) -> 9*
    add0(1,1) -> 9*
    add0(1,3) -> 9*
    add0(1,5) -> 9*
    add0(2,2) -> 9*
    add0(2,4) -> 9*
    first0(3,1) -> 10*
    first0(3,3) -> 10*
    first0(3,5) -> 10*
    first0(4,2) -> 10*
    first0(4,4) -> 10*
    first0(5,1) -> 10*
    first0(5,3) -> 10*
    first0(5,5) -> 10*
    first0(1,2) -> 10*
    first0(1,4) -> 10*
    first0(2,1) -> 10*
    first0(2,3) -> 10*
    first0(2,5) -> 10*
    first0(3,2) -> 10*
    first0(3,4) -> 10*
    first0(4,1) -> 10*
    first0(4,3) -> 10*
    first0(4,5) -> 10*
    first0(5,2) -> 10*
    first0(5,4) -> 10*
    first0(1,1) -> 10*
    first0(1,3) -> 10*
    first0(1,5) -> 10*
    first0(2,2) -> 10*
    first0(2,4) -> 10*
    nil0() -> 5*
    1 -> 9*
    2 -> 9*
    3 -> 9*
    4 -> 9*
    5 -> 9*
  problem:
   
  Qed